es:ES, e:E. es-height(es;e)   

latex

Definitions	x:A. B(x), E, P  Q, A  B, f(a), t  T, , es-height(es;e), ES, SWellFounded(R(x;y)), x:A. B(x), x:A  B(x), a < b, sender(e), n - m, #$n, pred(e), , n+m, -n, i  j , left + right, Unit, P  Q, P & Q, , Void, if b then t else f fi , i <z j, t.1, isrcv(e), , A, False, {x:A| B(x)} , b, s = t, x:AB(x)
Lemmas	es-sender wf, es-pred-causl, lt int wf, ifthenelse wf, es-sender-causl, es-pred wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, nat properties, ge wf, nat wf, le wf, es-causl-swellfnd